$\forall$$E$:Type$_{\mbox{\scriptsize i}}$, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $X_{1}$, $X_{2}$:Type$_{\mbox{\scriptsize i}}$, ${\it info}$:($E$$\rightarrow$(Id$\times$$X_{1}$+(IdLnk$\times$$E$)$\times$$X_{2}$)).
\\[0ex]EOrderAxioms\{i\}($E$;  ${\it pred?}$;${\it info}$) $\in$ Prop$_{\mbox{\scriptsize i'}}$